Section: New Results

Full Abstraction for Call-by-Value Programs with Choice

Participant : Jean Goubault-Larrecq.

Consider a programming language, with both an operational semantics, stating how one can implement a machine for this language, and a denotational semantics, which states what programs compute (not how). A classical question in programming language semantics is whether equality of denotations (from denotational semantics) coincides with contextual equivalence (from operational semantics). This is called full abstraction.

This question was first formulated for PCF by G. Plotkin in 1977, who showed that PCF was not fully abstract, although PCF plus a form of parallel or was. PCF is a simply-typed higher-order language, which one could see as a simple variant of the ML language without mutable state.

Jean Goubault-Larrecq examined the question for variants of PCF with various forms of non-deterministic and probabilistic choice. The latter are modeled denotationally by using his theory of previsions [61] . The most startling result is that the call-by-value variant of PCF with only angelic non-determinism is fully abstract, without the need for parallel or. Jean Goubault-Larrecq also showed that call-by-value PCF with angelic non-determinism and probabilistic choice is not fully abstract, but that this language plus so-called statistical test primitives is fully abstract. These results were presented at the Domains X Workshop, Swansea, Wales, UK, September 2011.